(declare-fun _substvar_1461_ () Bool)
(declare-fun _substvar_1463_ () Bool)
(declare-fun _substvar_1837_ () Bool)
(declare-const v1 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const i6 Int)
(declare-const arr-5443657655410947875_5443657655410947875-0 (Array Bool Bool))
(declare-const arr--8085496445804091638_5443657655410947875-0 (Array (Array Bool Bool) Bool))
(declare-const arr-8353079354350911363_5443657655410947875-0 (Array (Array (Array Bool Bool) Bool) Bool))
(assert (=> (select arr--8085496445804091638_5443657655410947875-0 arr-5443657655410947875_5443657655410947875-0) v7))
(assert (or _substvar_1463_ _substvar_1461_ (= (store arr-8353079354350911363_5443657655410947875-0 arr--8085496445804091638_5443657655410947875-0 false) (store arr-8353079354350911363_5443657655410947875-0 arr--8085496445804091638_5443657655410947875-0 (and v1 (< i6 27) (and v1 v8 _substvar_1837_) v7)) arr-8353079354350911363_5443657655410947875-0 arr-8353079354350911363_5443657655410947875-0)))
(check-sat)
